package probsym.heap;

import gov.nasa.jpf.symbc.Debug;
import gov.nasa.jpf.symbc.Symbolic;
import gov.nasa.jpf.symbc.probsym.Analyze;

public class Node {
   
    @Symbolic("true")
    int elem;
    Node next;

    Node createNode() {
        return next;
    }

    void setElem(int e) {
       
        this.elem = e;

    }
   
    Node swapNode() {
        if (this.next != null)
            if (elem > next.elem) {
                System.out.println("PC1 ");
            } else {
                System.out.println("PC2");
            }
        return this;
    }

    public static void main(String[] args) {
        Node X = new Node();
        //X.setElem(1);
        Node Y = new Node();
        Y= (Node) Debug.makeSymbolicRef("input_Y", Y);
        X = (Node) Debug.makeSymbolicRef("input_X", X);        
        //Y.setElem(1);
       
        //X.next = Y;
        //X.next.next = X;
       
        if (X != null) {
            X.swapNode();
        }
        Analyze.coverage(""+1);
        Debug.printSymbolicRef(X, "node = ");
        Debug.printHeapPC("2 HeapPC: ");
        Debug.printPC("PATH_CONDITION: ");
        Debug.printSymbolicRef(X, "return path condition:");
        System.out.println("*****************");

    }

}